Language/OS - Multiplatform Resource Library

home *** CD-ROM | disk | FTP | other *** search

/ Language/OS - Multiplatform Resource Library / LANGUAGE OS.iso / ast_comp / concurre.tar / concurrency / monoidal.tex / node8_mn.html < prev next >

Wrap

Text File | 1993-07-05 | 28KB | 349 lines

<H1><A ID="SECTION00040000000000000000"> CONCURRENCY</A> </H1> This section presents an attempt to relate the monoidal closed category of stable event structures to the category of event structures for modeling concurrency. We show that there is an adjunction between the two categories when the event structures are restricted to coherent spaces. We also indicate where the difficulty is in trying to generalize this result. A coherent space is a special kind of stable event structure <tex2html_verbatim_mark>#math222#(E, Con, <tex2html_image_mark>#tex2html_wrap_inline3507# ) where Con is determined by a symmetric, irreflexive relation # (the conflict relation), and <tex2html_image_mark>#tex2html_wrap_inline3511# is trivial in the sense that for every event e∈E, we have <tex2html_verbatim_mark>#math223#∅ <tex2html_image_mark>#tex2html_wrap_inline3514# e. Thus we say a set of events X consistent if <tex2html_verbatim_mark>#math224#∀e, e'∈X. ¬(e#e'). For technical reasons, here we allow E to be any set. It is convenient to write a coherent space in the form (E,#) since the enabling relation is trivial. It is well-known that coherent spaces with linear maps form a monoidal closed category. The linear maps are exactly the same as those on stable event structures (but restricted to coherent spaces). <DIV><#3520#>Definition 4.1<#3520#> <#3523#>Let <tex2html_verbatim_mark>#math225#<tex2html_image_mark>#tex2html_wrap_inline3525# = (E0,#0), <tex2html_verbatim_mark>#math226#<tex2html_image_mark>#tex2html_wrap_inline3527# = (E1,#1) be coherent spaces. A linear map from <tex2html_verbatim_mark>#math227#<tex2html_image_mark>#tex2html_wrap_inline3529# to <tex2html_verbatim_mark>#math228#<tex2html_image_mark>#tex2html_wrap_inline3531# is a relation <tex2html_verbatim_mark>#math229#R⊆E0×E1 which satisfies <tex2html_verbatim_mark>#math230#<DIV ALIGN="CENTER"> <TABLE> <TR VALIGN="MIDDLE"><TD ALIGN="LEFT">1. (e0Re1 <tex2html_ampersand_mark> e0'Re1' <tex2html_ampersand_mark> e1#e1') <tex2html_image_mark>#tex2html_wrap_indisplay3535# e0#e0',</TD> </TR> <TR VALIGN="MIDDLE"><TD ALIGN="LEFT">2. [e0Re <tex2html_ampersand_mark> e0'Re <tex2html_ampersand_mark> ¬(e0#e0')] <tex2html_image_mark>#tex2html_wrap_indisplay3537# e0 = e0'.</TD> </TR> </TABLE> </DIV><#3523#></DIV> Note that the completeness axiom as required for a linear map (see Definition 3.5) is vacuously true. The category of event structures which gives non-interleaving semantics to concurrent languages like CCS has a different kind of morphisms: the <#520#>partially synchronous morphisms<#520#> [Wi87], [Wi88]. There are constructions of product and coproduct in this category, which are used to model parallel composition and nondeterministic choices of CCS like processes. Originally the objects of this category are stable event structures. When restricted to coherent spaces, partially synchronous morphisms can be simplified as follows. <DIV><#3539#>Definition 4.2<#3539#> <#3542#>Let <tex2html_verbatim_mark>#math231#<tex2html_image_mark>#tex2html_wrap_inline3544# = (E0,#0), <tex2html_verbatim_mark>#math232#<tex2html_image_mark>#tex2html_wrap_inline3546# = (E1,#1) be coherent spaces. A partially synchronous morphism from <tex2html_verbatim_mark>#math233#<tex2html_image_mark>#tex2html_wrap_inline3548# to <tex2html_verbatim_mark>#math234#<tex2html_image_mark>#tex2html_wrap_inline3550# is a partial function <tex2html_verbatim_mark>#math235#θ : E0→E1 which satisfies <tex2html_verbatim_mark>#math236#<DIV ALIGN="CENTER"> <TABLE> <TR VALIGN="MIDDLE"><TD ALIGN="LEFT">1. θ(e)#θ(e') <tex2html_image_mark>#tex2html_wrap_indisplay3554# e#e',</TD> </TR> <TR VALIGN="MIDDLE"><TD ALIGN="LEFT">2. [θ(e) = θ(e') <tex2html_ampersand_mark> ¬(e#e')] <tex2html_image_mark>#tex2html_wrap_indisplay3556# e = e'.</TD> </TR> </TABLE> </DIV><#3542#></DIV> Note that by convention when we write <tex2html_verbatim_mark>#math237#θ(e)#θ(e') or <tex2html_verbatim_mark>#math238#θ(e) = θ(e'), <tex2html_verbatim_mark>#math239#θ(e) and <tex2html_verbatim_mark>#math240#θ(e') are both defined. Comparing the definition of a linear map to that of a partially synchronous morphism, one can see that partially synchronous morphisms are special kind of linear maps. The only difference between these two notions is that a linear map is determined by a relation, while a partially synchronous morphism is determined by a partial function. The reason for using a (partial) function for a partially synchronous morphism may be traced back to the synchronization mechanism for CCS processes. The synchronization of two CCS processes is achieved by communication through handshake, an indivisible action in which a message is simultaneously emitted by one process and received by the other [Mi89]. Handshakes happen between two parties only. CCS does not allow a party to handshake with more than one party at a given time. Therefore, the `communication partner of' a process determines a partial function. From a concurrency point of view, a linear map supports the synchronization of more than two events. Two pairs of events <tex2html_verbatim_mark>#math241#( e, e1 ), <tex2html_verbatim_mark>#math242#( e, e2 ) in the relation R can be understood as the synchronization of the event e with e1 and e2. There are many practical examples of synchronization among more than two parties. A conference call enabled by a telephone company is one such example. However, linear maps seem to allow more than that. Potentially, one event can synchronize with infinitely many other events. Consider the following sequence of relations between a coherent space with a single event e and one with the event set ω and the empty conflict relation: <tex2html_verbatim_mark>#math243#<DIV ALIGN="CENTER"> <TABLE> <TR VALIGN="MIDDLE"><TD ALIGN="LEFT">R0 = ∅,</TD> </TR> <TR VALIGN="MIDDLE"><TD ALIGN="LEFT">R1 = {(e, 0)},</TD> </TR> <TR VALIGN="MIDDLE"><TD ALIGN="LEFT"> ... ,</TD> </TR> <TR VALIGN="MIDDLE"><TD ALIGN="LEFT">Ri = {(e, j) | j ;SPMlt; i},</TD> </TR> <TR VALIGN="MIDDLE"><TD ALIGN="LEFT"> ... </TD> </TR> </TABLE> </DIV> Each Ri corresponds to a linear map, and the subset relation on them specifies the stable order. Therefore, the least upper bound (in the linear function space) of the sequence Ri is <tex2html_verbatim_mark>#math244#{(e, j) | j∈ω}. Our purpose is to establish an adjunction between the category of coherent spaces with partial synchronous morphisms (written as <#534#>CPS<#534#>) and the category of coherent spaces with linear maps (written as <#535#>CLI<#535#>). The foregoing discussions suggest that we should find a construction <tex2html_image_mark>#tex2html_wrap_inline3579# on coherent spaces <tex2html_verbatim_mark>#math245#<tex2html_image_mark>#tex2html_wrap_inline3581# such that <tex2html_verbatim_mark>#math246#<DIV ALIGN="CENTER"> <tex2html_image_mark>#tex2html_wrap_indisplay3583#→lin<tex2html_image_mark>#tex2html_wrap_indisplay3584#≅<tex2html_image_mark>#tex2html_wrap_indisplay3585#→ps(<tex2html_image_mark>#tex2html_wrap_indisplay3586#<tex2html_image_mark>#tex2html_wrap_indisplay3587#), </DIV> where <tex2html_verbatim_mark>#math247#<tex2html_image_mark>#tex2html_wrap_inline3589#→lin<tex2html_image_mark>#tex2html_wrap_inline3590# stands for the set of linear maps from <tex2html_verbatim_mark>#math248#<tex2html_image_mark>#tex2html_wrap_inline3592# to <tex2html_verbatim_mark>#math249#<tex2html_image_mark>#tex2html_wrap_inline3594#, and <tex2html_verbatim_mark>#math250#<tex2html_image_mark>#tex2html_wrap_inline3596#→ps(<tex2html_image_mark>#tex2html_wrap_inline3597#<tex2html_image_mark>#tex2html_wrap_inline3598#) stands for the set of partial synchronous morphisms form <tex2html_verbatim_mark>#math251#<tex2html_image_mark>#tex2html_wrap_inline3600# to <tex2html_verbatim_mark>#math252#<tex2html_image_mark>#tex2html_wrap_inline3602#<tex2html_image_mark>#tex2html_wrap_inline3603#. With respect to the example mentioned in the previous paragraph, the linear map <tex2html_verbatim_mark>#math253#{(e, j) | j∈ω} should correspond to some kind of partial synchronous morphism <tex2html_verbatim_mark>#math254#{(e, ω)}. This implies that the events of <tex2html_verbatim_mark>#math255#<tex2html_image_mark>#tex2html_wrap_inline3607#<tex2html_image_mark>#tex2html_wrap_inline3608# should be non-empty, consistent subsets of E1 -- not merely finite consistent subsets. This is exactly the technical reason that takes us out of countable event sets. <DIV><#3611#>Definition 4.3<#3611#> <#3614#>Let <tex2html_verbatim_mark>#math256#<tex2html_image_mark>#tex2html_wrap_inline3616# = (E,#) be a coherent space. Define <tex2html_verbatim_mark>#math257#<tex2html_image_mark>#tex2html_wrap_inline3618#<tex2html_image_mark>#tex2html_wrap_inline3619# to be the coherent space <tex2html_verbatim_mark>#math258#(E',#'), where <tex2html_verbatim_mark>#math259#<DIV ALIGN="CENTER"> <TABLE> <TR VALIGN="MIDDLE"><TD ALIGN="LEFT">E' = {x | x⊆E <tex2html_ampersand_mark> x <tex2html_image_mark>#tex2html_wrap_indisplay3623#∅ <tex2html_ampersand_mark> ∀e, e'∈x.¬(e#e')},</TD> </TR> <TR VALIGN="MIDDLE"><TD ALIGN="LEFT">x#'y <tex2html_image_mark>#tex2html_wrap_indisplay3625# [(x∩y <tex2html_image_mark>#tex2html_wrap_indisplay3626#∅ <tex2html_ampersand_mark> x <tex2html_image_mark>#tex2html_wrap_indisplay3627#y) or ∃e∈x∃e'∈y.e#e'].</TD> </TR> </TABLE> </DIV><#3614#></DIV> Now we are in a position to prove the following theorem. <DIV><#3629#>Theorem 4.1<#3629#> <#3632#>For coherent spaces <tex2html_verbatim_mark>#math260#<tex2html_image_mark>#tex2html_wrap_inline3634# = (E0,#0) and <tex2html_verbatim_mark>#math261#<tex2html_image_mark>#tex2html_wrap_inline3636# = (E1,#1), we have <tex2html_verbatim_mark>#math262#<DIV ALIGN="CENTER"> <tex2html_image_mark>#tex2html_wrap_indisplay3638#→lin<tex2html_image_mark>#tex2html_wrap_indisplay3639#≅<tex2html_image_mark>#tex2html_wrap_indisplay3640#→ps(<tex2html_image_mark>#tex2html_wrap_indisplay3641#<tex2html_image_mark>#tex2html_wrap_indisplay3642#). </DIV><#3632#></DIV> <#575#>Proof <#575#> For any linear map <tex2html_verbatim_mark>#math263#R : <tex2html_image_mark>#tex2html_wrap_inline3644#→<tex2html_image_mark>#tex2html_wrap_inline3645#, let <tex2html_verbatim_mark>#math264#<DIV ALIGN="CENTER"> f (R) : E0→{x | x⊆E <tex2html_ampersand_mark> x <tex2html_image_mark>#tex2html_wrap_indisplay3647#∅ <tex2html_ampersand_mark> ∀e, e'∈x.¬(e#e')} </DIV> be a partial function such that f (R)(e) is defined to be <tex2html_verbatim_mark>#math265#{e' | e'∈E1 <tex2html_ampersand_mark> eRe'} if it is not empty. Clearly f (R)(e) is consistent. We show that f (R) is a partially synchronous morphism from <tex2html_verbatim_mark>#math266#<tex2html_image_mark>#tex2html_wrap_inline3653# to <tex2html_verbatim_mark>#math267#<tex2html_image_mark>#tex2html_wrap_inline3655#<tex2html_image_mark>#tex2html_wrap_inline3656#. Assume <tex2html_verbatim_mark>#math268#f (R)(e)#f (R)(e'). By Definition 4.3, either there exist <tex2html_verbatim_mark>#math269#a∈f (R)(e) and <tex2html_verbatim_mark>#math270#b∈f (R)(e') such that a#1b, or f (R)(e) and f (R)(e') are different sets with a non-empty intersection. For the first case we have e#0e', by the properties of R. For the second case, there must be an a∈E1 such that eRa and e'Ra. Again by the properties of R, we must have e#0e' since <tex2html_verbatim_mark>#math271#f (R)(e) <tex2html_image_mark>#tex2html_wrap_inline3671#f (R)(e') implies <tex2html_verbatim_mark>#math272#e <tex2html_image_mark>#tex2html_wrap_inline3673#e'. We also have <tex2html_verbatim_mark>#math273#<DIV ALIGN="CENTER"> [f (R)(e) = f (R)(e') <tex2html_ampersand_mark> ¬(e#0e')] <tex2html_image_mark>#tex2html_wrap_indisplay3675# e = e' </DIV> since <tex2html_verbatim_mark>#math274#f (R)(e) = f (R)(e') implies the non-emptyness of f (R)(e). Therefore, f (R) is indeed a partially synchronous morphism. On the other hand, for any partially synchronous morphism <tex2html_verbatim_mark>#math275#θ : <tex2html_image_mark>#tex2html_wrap_inline3680#→<tex2html_image_mark>#tex2html_wrap_inline3681#<tex2html_image_mark>#tex2html_wrap_inline3682#, let <tex2html_verbatim_mark>#math276#g(θ)⊆E0→E1 be a relation such that <tex2html_verbatim_mark>#math277#(e, e')∈g(θ) if and only if <tex2html_verbatim_mark>#math278#e'∈θ(e). We show that <tex2html_verbatim_mark>#math279#g(θ) is a linear map from <tex2html_verbatim_mark>#math280#<tex2html_image_mark>#tex2html_wrap_inline3688# to <tex2html_verbatim_mark>#math281#<tex2html_image_mark>#tex2html_wrap_inline3690#. Assume <tex2html_verbatim_mark>#math282#(e0, e1),(e0', e1')∈g(θ) and <tex2html_verbatim_mark>#math283#e1#1e1'. By Definition 4.3, <tex2html_verbatim_mark>#math284#θ(e0)#θ(e0'). Since θ is a partially synchronous morphism, we have <tex2html_verbatim_mark>#math285#e0#0e0'. We now check that <tex2html_verbatim_mark>#math286#<DIV ALIGN="CENTER"> [(e0, e),(e0', e)∈g(θ) <tex2html_ampersand_mark> ¬(e0#1e0')] <tex2html_image_mark>#tex2html_wrap_indisplay3697# e0 = e0'. </DIV> This is because the given conditions imply <tex2html_verbatim_mark>#math287#θ(e0)∩θ(e0') <tex2html_image_mark>#tex2html_wrap_inline3699#∅ and <tex2html_verbatim_mark>#math288#¬(θ(e0)#θ(e0'). This is only possible when <tex2html_verbatim_mark>#math289#θ(e0) = θ(e0'), which in turn implies e0 = e0'. It is now a relatively easy task to check that f and g indeed give rise to the desired isomorphism. <tex2html_image_mark>#tex2html_wrap_inline3706# The consequence of this result, put in categorical terms, is that the forgetful functor <tex2html_verbatim_mark>#math290#U : <tex2html_image_mark>#tex2html_wrap_inline3708#→<tex2html_image_mark>#tex2html_wrap_inline3709# has a left adjoint <tex2html_verbatim_mark>#math291#F : <tex2html_image_mark>#tex2html_wrap_inline3711#→<tex2html_image_mark>#tex2html_wrap_inline3712# as specified below. <DIV><#3714#>Theorem 4.2<#3714#> <#3717#>The forgetful functor <tex2html_verbatim_mark>#math292#U : <tex2html_image_mark>#tex2html_wrap_inline3719#→<tex2html_image_mark>#tex2html_wrap_inline3720# has the left adjoint <tex2html_verbatim_mark>#math293#F : <tex2html_image_mark>#tex2html_wrap_inline3722#→<tex2html_image_mark>#tex2html_wrap_inline3723# where <tex2html_verbatim_mark>#math294#F(<tex2html_image_mark>#tex2html_wrap_inline3725#) = <tex2html_image_mark>#tex2html_wrap_inline3726#<tex2html_image_mark>#tex2html_wrap_inline3727#, and <tex2html_verbatim_mark>#math295#<DIV ALIGN="CENTER"> F(R)(x) = {e' | ∃e∈x.(e, e')∈R} </DIV> for a linear map <tex2html_verbatim_mark>#math296#R : <tex2html_image_mark>#tex2html_wrap_inline3730#→<tex2html_image_mark>#tex2html_wrap_inline3731#.<#3717#></DIV> <#600#>Proof <#600#> This follows from the previous theorem and the fact that <tex2html_verbatim_mark>#math297#F(R) : F(<tex2html_image_mark>#tex2html_wrap_inline3733#→F(<tex2html_image_mark>#tex2html_wrap_inline3734#) is a partially synchronous morphism for any linear map <tex2html_verbatim_mark>#math298#R : <tex2html_image_mark>#tex2html_wrap_inline3736#→<tex2html_image_mark>#tex2html_wrap_inline3737#. <tex2html_image_mark>#tex2html_wrap_inline3739# Since left adjoints preserve colimits such as coproducts, categories <#605#>CLI<#605#> and <#606#>CPS<#606#> have the same sum construction for modeling non-deterministic choices of CCS processes. The obvious next step is to extend the adjunction to stable event structures. To make things simpler, we work on prime event structures first. Recall that a prime event structure is a triple <tex2html_verbatim_mark>#math299#<tex2html_image_mark>#tex2html_wrap_inline3741# = (E, Con,≤), where E is a set of events, partially ordered by ≤, and Con is a consistency predicate which is downwards closed with respect to ≤ (the causal dependency order): <tex2html_verbatim_mark>#math300#<DIV ALIGN="CENTER"> (X∈Con <tex2html_ampersand_mark> e≤e'∈X) <tex2html_image_mark>#tex2html_wrap_indisplay3747# X∪{e}∈Con. </DIV> Moreover, for any e∈E, the set <tex2html_verbatim_mark>#math301#⌈⌈e⌉⌉ = {e' | e'≤e <tex2html_ampersand_mark> e <tex2html_image_mark>#tex2html_wrap_inline3750#e'} is finite. Our work in Section 3 can be easily extended to prime event structures. There is a monoidal closed category with the following linear maps as morphisms. <DIV><#3752#>Definition 4.4<#3752#> <#3755#>Let <tex2html_verbatim_mark>#math302#<tex2html_image_mark>#tex2html_wrap_inline3757# = ( E, Con<tex2html_image_mark>#tex2html_wrap_inline3758#, <tex2html_image_mark>#tex2html_wrap_inline3759# ), <tex2html_image_mark>#tex2html_wrap_inline3760# = ( F, Con<tex2html_image_mark>#tex2html_wrap_inline3761#, <tex2html_image_mark>#tex2html_wrap_inline3762# ) be prime event structures. A linear map from <tex2html_verbatim_mark>#math303#<tex2html_image_mark>#tex2html_wrap_inline3764# to <tex2html_verbatim_mark>#math304#<tex2html_image_mark>#tex2html_wrap_inline3766# is a relation <tex2html_verbatim_mark>#math305#R⊆E×F which satisfies <tex2html_verbatim_mark>#math306#<DIV ALIGN="CENTER"> <tex2html_image_mark>#tex2html_wrap_indisplay3769#<tex2html_image_mark>#tex2html_wrap_indisplay3770#1<tex2html_image_mark>#tex2html_wrap_indisplay3771#<tex2html_image_mark>#tex2html_wrap_indisplay3772#=0pt<tex2html_image_mark>#tex2html_wrap_indisplay3773#$##$ ;SPMamp; $## $<tex2html_image_mark>#tex2html_wrap_indisplay3774# ;SPMamp; 1.Compatibility:( ∀i∈I . ei R ei' ) <tex2html_ampersand_mark> {ei | i∈I}∈Con<tex2html_image_mark>#tex2html_wrap_indisplay3775# <tex2html_image_mark>#tex2html_wrap_indisplay3776# { ei' | i∈I }∈Con<tex2html_image_mark>#tex2html_wrap_indisplay3777#,<tex2html_image_mark>#tex2html_wrap_indisplay3778# ;SPMamp; 2.Minimality:( {e0, e1}∈Con<tex2html_image_mark>#tex2html_wrap_indisplay3779# <tex2html_ampersand_mark> e0 R e <tex2html_ampersand_mark> e1 R e ) <tex2html_image_mark>#tex2html_wrap_indisplay3780# e0=e1, and<tex2html_image_mark>#tex2html_wrap_indisplay3781# ;SPMamp; 3.Completeness:e R e' <tex2html_image_mark>#tex2html_wrap_indisplay3782# ∀e1'∈⌈⌈e'⌉⌉∃e0'≤e. e0' R e1'.<tex2html_image_mark>#tex2html_wrap_indisplay3783#<tex2html_image_mark>#tex2html_wrap_indisplay3784# </DIV> Here I is a finite index set.<#3755#></DIV> The definition of partially synchronous morphisms is almost the same on prime event structures as on stable event structures, if one recovers the enabling relation by letting <tex2html_verbatim_mark>#math307#<DIV ALIGN="CENTER"> X <tex2html_image_mark>#tex2html_wrap_indisplay3787# e ifandonlyif ⌈⌈e⌉⌉⊆X. </DIV> <DIV><#3789#>Definition 4.5<#3789#> <#3792#>Let <tex2html_verbatim_mark>#math308#<tex2html_image_mark>#tex2html_wrap_inline3794# = ( E1, Con1, ≤1 ) and <tex2html_verbatim_mark>#math309#<tex2html_image_mark>#tex2html_wrap_inline3796# = (E2, Con2, ≤2) be prime event structures. A partially synchronous morphism from <tex2html_verbatim_mark>#math310#<tex2html_image_mark>#tex2html_wrap_inline3798# to <tex2html_verbatim_mark>#math311#<tex2html_image_mark>#tex2html_wrap_inline3800# is a partial function <tex2html_verbatim_mark>#math312#θ : E1→E2 on on events which satisfies <tex2html_verbatim_mark>#math313#<DIV ALIGN="CENTER"> <TABLE> <TR VALIGN="MIDDLE"><TD ALIGN="LEFT"> </TD> <TD ALIGN="LEFT">• X∈Con1 <tex2html_image_mark>#tex2html_wrap_indisplay3805# θX∈Con2,</TD> </TR> <TR VALIGN="MIDDLE"><TD ALIGN="LEFT"> </TD> <TD ALIGN="LEFT">• ({ e, e' }∈Con1 <tex2html_ampersand_mark> θ(e) = θ(e')) <tex2html_image_mark>#tex2html_wrap_indisplay3808# e = e', and</TD> </TR> <TR VALIGN="MIDDLE"><TD ALIGN="LEFT"> </TD> <TD ALIGN="LEFT">• θ(e) isdefined <tex2html_image_mark>#tex2html_wrap_indisplay3811# ⌈⌈θ(e)⌉⌉⊆θ⌈⌈e⌉⌉.</TD> </TR> </TABLE> </DIV><#3792#></DIV> To get an adjunction between the category of prime event structures with linear maps and the category of prime event structures with partially synchronous morphisms, a construction <tex2html_image_mark>#tex2html_wrap_inline3813# similar to the one on coherent spaces seems necessary. For a prime event structure <tex2html_verbatim_mark>#math314#<tex2html_image_mark>#tex2html_wrap_inline3815#, the events of <tex2html_verbatim_mark>#math315#<tex2html_image_mark>#tex2html_wrap_inline3817#<tex2html_image_mark>#tex2html_wrap_inline3818# should be non-empty subsets of E. The definition of the consistency relation on <tex2html_verbatim_mark>#math316#<tex2html_image_mark>#tex2html_wrap_inline3821#<tex2html_image_mark>#tex2html_wrap_inline3822# is similar to the one for coherent spaces. However, it is unclear to me at this moment how to get the appropriate definition of a causal dependency order on subsets of E so that a similar isomorphism as the one in Theorem 4.1 exists. None of the partial orders for powerdomains seems to work here, and the difficulty seems to be in making sure <tex2html_verbatim_mark>#math317#<tex2html_image_mark>#tex2html_wrap_inline3825#<tex2html_image_mark>#tex2html_wrap_inline3826# is a prime event structure. It could well be that everything works fine on stable event structures. However, we have to leave that as a research topic.